(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun q () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun r () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(assert (not (exists ((o Real)) (= (and (or (and (and (or (or (and (< (- (/ (* q q) 0)) h 0.0 f)) (<= 0.0 q)) (<= q (/ 10 d)))) (<= r 0)))) (or (= true (= (= (and (<= o (- b))) (and (and (<= 0.0 (+ (* e o) g))) (= (+ (- e o) g) 0))) false)))))))
(assert (or (exists ((p Real)) (= (or (and (or (and (or (and (and (and (and (=> (and (<= 0 i)) (and (and (<= 0.0 (/ (+ 0 l) (- a q)) 0)) (<= 0 m)))))) (= n 2.0)))))) (< 0.0 m)) false))))
(assert (= a (* q k)))
(assert (distinct c (/ f k h j)))
(check-sat)
